L’équipe VELO étudie les méthodes formelles permettant la modélisation et l’analyse de modèles pour les systèmes complexes. Ces systèmes peuvent être de tous types, mais nous nous intéressons plus particulièrement à la modélisation de systèmes naturels à grande échelle (issus de l’environnement) et de systèmes logiciels. Nos principaux objets d'étude sont les modèles, quelle que soit leur origine. Nous étudions et développons ainsi des formalismes de modélisation adaptés aux contextes dans lequels nos systèmes évoluent (semi-formels, formels, à évènements discrets, continus, probabilistes, hybrides, etc.), ainsi que les techniques de vérification associées (test logiciel, preuve formelle, model-checking, analyse statistique).

Les systèmes complexes qui font interagir des composants physiques ou logiciels variés, d'importantes données, des contraintes de temps, des exigences de robustesse et de qualité sont difficiles à modéliser et à développer.
 
Nous attaquons ces difficultés à travers différentes thématiques qui gravitent autour des modèles, de leur construction à leur analyse. L'étude des modèles est alors déclinée selon différentes facettes qui constituent un système complexe :

• Les agents/services et composants qui interagissent dans le système ;
• L'analyse des systèmes hétérogènes ;
• L'architecture et l'évolution du système ;
• Les modèles sémantiques variés (par exemple, des modèles logiques, à états, à composants, à services, à événements discrets, probabilistes, temporisés) et les techniques de vérification associées.

• Composants logiciel corrects
• Multiformalisme et analyse multifacette des systèmes complexes
• Architecture logicielle
• Modèles probabilistes, sémantiques de la concurrence, outils de vérification associés.

Par rapport à ces thématiques, les compétences des membres de l'équipe nous permettent d'explorer en particulier :

• les modèles pour les services, composants et l'architecture globale ;
• les méthodes de vérification par la preuve, l'exploration d'états et le test ;
• les systèmes réactifs, concurrents, embarqués et les systèmes d'information ;
• les systèmes naturels à comportement continu ou hybride.